Conversation
| run: | | ||
| echo "TEST_ARGS='--wfail --iofail'" >> $GITHUB_ENV | ||
| shell: bash | ||
| - uses: leanprover/lean-action@v1 |
There was a problem hiding this comment.
I think you can also change the v1 and possibly the username here to point at the commit with the fix
There was a problem hiding this comment.
I'd be happy to point to a specific commit in the lean-action repo once the fix lands, but I'm not sure we should point to individual usernames in CI if at all avoidable. I was initially of the opinion that sticking to v1 seemed fine as this does pick up new minor releases, but the PR adding test-args (where I was the one who introduced the bug...) took ~5 months to land in a release,
There was a problem hiding this comment.
If you point to a specific git hash then I think the risk of pointing to an external user goes away.
|
Merging this in the meantime, but let's keep an eye on future upstream fixes in the action. |
Pending leanprover/lean-action#153, manually set `TEST_ARGS`. As can be seen from the CI runs, this now correctly results in running `lake test --wfail --iofail`.
3 participants
Pending leanprover/lean-action#153, manually set
TEST_ARGS. As can be seen from the CI runs, this now correctly results in runninglake test --wfail --iofail.